circuit Top :
  extmodule ResetCounter :
    input clk : Clock
    input reset : UInt<1>
    output timeSinceReset : UInt<32>
    output notChaos : UInt<1>
    defname = ResetCounter

  module Top :
    input clock : Clock
    input reset : UInt<1>
    output io : { flip in_wr : UInt<1>, flip in_wdata : UInt<512>, flip in_rd : UInt<1>, out_rdata : UInt<512>, out_empty : UInt<1>, out_full : UInt<1>, flip rnd_mark : UInt<1>}

    inst resetCounter of ResetCounter @[Formal.scala 10:36]
    resetCounter.notChaos is invalid
    resetCounter.timeSinceReset is invalid
    resetCounter.reset is invalid
    resetCounter.clk is invalid
    resetCounter.clk <= clock @[Formal.scala 11:23]
    resetCounter.reset <= reset @[Formal.scala 12:25]
    cmem buffer : UInt<512> [4] @[Top.scala 22:19]
    reg wrptr : UInt<2>, clock with :
      reset => (reset, UInt<2>("h0")) @[Top.scala 23:22]
    reg rdptr : UInt<2>, clock with :
      reset => (reset, UInt<2>("h0")) @[Top.scala 24:22]
    node _pdiff_T = add(wrptr, UInt<1>("h1")) @[Top.scala 25:32]
    node _pdiff_T_1 = tail(_pdiff_T, 1) @[Top.scala 25:32]
    node pdiff = eq(rdptr, _pdiff_T_1) @[Top.scala 25:22]
    reg out_rdata : UInt<512>, clock with :
      reset => (reset, UInt<512>("h0")) @[Top.scala 27:26]
    io.out_rdata <= out_rdata @[Top.scala 28:16]
    reg out_full : UInt<1>, clock with :
      reset => (reset, UInt<1>("h0")) @[Top.scala 30:25]
    io.out_full <= out_full @[Top.scala 31:15]
    node _io_out_empty_T = eq(wrptr, rdptr) @[Top.scala 34:26]
    node _io_out_empty_T_1 = not(out_full) @[Top.scala 34:39]
    node _io_out_empty_T_2 = and(_io_out_empty_T, _io_out_empty_T_1) @[Top.scala 34:37]
    io.out_empty <= _io_out_empty_T_2 @[Top.scala 34:16]
    node _T = and(pdiff, io.in_wr) @[Top.scala 37:14]
    node _T_1 = eq(io.in_rd, UInt<1>("h0")) @[Top.scala 37:29]
    node _T_2 = and(_T, _T_1) @[Top.scala 37:26]
    when _T_2 : @[Top.scala 37:39]
      out_full <= UInt<1>("h1") @[Top.scala 38:14]
    else :
      node _T_3 = eq(io.in_wr, UInt<1>("h0")) @[Top.scala 39:15]
      node _T_4 = and(_T_3, io.in_rd) @[Top.scala 39:25]
      when _T_4 : @[Top.scala 39:37]
        out_full <= UInt<1>("h0") @[Top.scala 40:14]
      else :
        out_full <= out_full @[Top.scala 42:14]
    when io.in_wr : @[Top.scala 46:17]
      node _T_5 = lt(wrptr, UInt<2>("h3")) @[Top.scala 47:16]
      when _T_5 : @[Top.scala 47:34]
        node _wrptr_T = add(wrptr, UInt<1>("h1")) @[Top.scala 48:22]
        node _wrptr_T_1 = tail(_wrptr_T, 1) @[Top.scala 48:22]
        wrptr <= _wrptr_T_1 @[Top.scala 48:13]
      else :
        wrptr <= UInt<2>("h0") @[Top.scala 50:13]
    else :
      wrptr <= wrptr @[Top.scala 53:11]
    when io.in_rd : @[Top.scala 57:17]
      node _T_6 = lt(rdptr, UInt<2>("h3")) @[Top.scala 58:16]
      when _T_6 : @[Top.scala 58:34]
        node _rdptr_T = add(rdptr, UInt<1>("h1")) @[Top.scala 59:22]
        node _rdptr_T_1 = tail(_rdptr_T, 1) @[Top.scala 59:22]
        rdptr <= _rdptr_T_1 @[Top.scala 59:13]
      else :
        rdptr <= UInt<2>("h0") @[Top.scala 61:13]
    else :
      rdptr <= rdptr @[Top.scala 64:11]
    when io.in_wr : @[Top.scala 68:18]
      write mport MPORT = buffer[wrptr], clock
      MPORT <= io.in_wdata
    when io.in_rd : @[Top.scala 73:17]
      read mport out_rdata_MPORT = buffer[rdptr], clock @[Top.scala 74:29]
      out_rdata <= out_rdata_MPORT @[Top.scala 74:15]
    else :
      out_rdata <= out_rdata @[Top.scala 76:15]
    when out_full : @[Top.scala 80:17]
      node _T_7 = eq(io.in_wr, UInt<1>("h0")) @[Top.scala 81:12]
      node _T_8 = bits(reset, 0, 0) @[Top.scala 81:11]
      node _T_9 = eq(_T_8, UInt<1>("h0")) @[Top.scala 81:11]
      when _T_9 : @[Top.scala 81:11]
        node _T_10 = eq(_T_7, UInt<1>("h0")) @[Top.scala 81:11]
        when _T_10 : @[Top.scala 81:11]
          printf(clock, UInt<1>("h1"), "Assumption failed\n    at Top.scala:81 assume(!io.in_wr)\n") : printf @[Top.scala 81:11]
        assume(clock, _T_7, UInt<1>("h1"), "") : assume @[Top.scala 81:11]
    when io.out_empty : @[Top.scala 83:21]
      node _T_11 = eq(io.in_rd, UInt<1>("h0")) @[Top.scala 84:12]
      node _T_12 = bits(reset, 0, 0) @[Top.scala 84:11]
      node _T_13 = eq(_T_12, UInt<1>("h0")) @[Top.scala 84:11]
      when _T_13 : @[Top.scala 84:11]
        node _T_14 = eq(_T_11, UInt<1>("h0")) @[Top.scala 84:11]
        when _T_14 : @[Top.scala 84:11]
          printf(clock, UInt<1>("h1"), "Assumption failed\n    at Top.scala:84 assume(!io.in_rd)\n") : printf_1 @[Top.scala 84:11]
        assume(clock, _T_11, UInt<1>("h1"), "") : assume_1 @[Top.scala 84:11]
    reg in_rd_ff1 : UInt<1>, clock with :
      reset => (reset, UInt<1>("h0")) @[Top.scala 87:26]
    reg flag : UInt<1>, clock with :
      reset => (reset, UInt<1>("h0")) @[Top.scala 88:21]
    wire rnd_mark : UInt<1> @[Top.scala 89:22]
    rnd_mark <= io.rnd_mark @[Top.scala 90:12]
    wire mark_vld : UInt<1> @[Top.scala 92:22]
    wire check_vld : UInt<1> @[Top.scala 93:23]
    node _mark_vld_T = and(io.in_wr, rnd_mark) @[Top.scala 95:24]
    mark_vld <= _mark_vld_T @[Top.scala 95:12]
    node _check_vld_T = eq(out_rdata, UInt<512>("h1")) @[Top.scala 96:39]
    node _check_vld_T_1 = and(in_rd_ff1, _check_vld_T) @[Top.scala 96:26]
    check_vld <= _check_vld_T_1 @[Top.scala 96:13]
    in_rd_ff1 <= io.in_rd @[Top.scala 98:13]
    when check_vld : @[Top.scala 100:18]
      flag <= UInt<1>("h0") @[Top.scala 101:10]
    else :
      when mark_vld : @[Top.scala 102:24]
        flag <= UInt<1>("h1") @[Top.scala 103:10]
    when mark_vld : @[Top.scala 106:17]
      node _T_15 = eq(io.in_wdata, UInt<512>("h1")) @[Top.scala 107:24]
      node _T_16 = bits(reset, 0, 0) @[Top.scala 107:11]
      node _T_17 = eq(_T_16, UInt<1>("h0")) @[Top.scala 107:11]
      when _T_17 : @[Top.scala 107:11]
        node _T_18 = eq(_T_15, UInt<1>("h0")) @[Top.scala 107:11]
        when _T_18 : @[Top.scala 107:11]
          printf(clock, UInt<1>("h1"), "Assumption failed\n    at Top.scala:107 assume(io.in_wdata === 1.U(WIDTH.W))\n") : printf_2 @[Top.scala 107:11]
        assume(clock, _T_15, UInt<1>("h1"), "") : assume_2 @[Top.scala 107:11]
    node _T_19 = eq(mark_vld, UInt<1>("h0")) @[Top.scala 109:8]
    node _T_20 = and(_T_19, io.in_wr) @[Top.scala 109:18]
    when _T_20 : @[Top.scala 109:30]
      node _T_21 = eq(io.in_wdata, UInt<512>("h0")) @[Top.scala 110:24]
      node _T_22 = bits(reset, 0, 0) @[Top.scala 110:11]
      node _T_23 = eq(_T_22, UInt<1>("h0")) @[Top.scala 110:11]
      when _T_23 : @[Top.scala 110:11]
        node _T_24 = eq(_T_21, UInt<1>("h0")) @[Top.scala 110:11]
        when _T_24 : @[Top.scala 110:11]
          printf(clock, UInt<1>("h1"), "Assumption failed\n    at Top.scala:110 assume(io.in_wdata === 0.U(WIDTH.W))\n") : printf_3 @[Top.scala 110:11]
        assume(clock, _T_21, UInt<1>("h1"), "") : assume_3 @[Top.scala 110:11]
    when flag : @[Top.scala 112:13]
      node _T_25 = eq(mark_vld, UInt<1>("h0")) @[Top.scala 113:12]
      node _T_26 = bits(reset, 0, 0) @[Top.scala 113:11]
      node _T_27 = eq(_T_26, UInt<1>("h0")) @[Top.scala 113:11]
      when _T_27 : @[Top.scala 113:11]
        node _T_28 = eq(_T_25, UInt<1>("h0")) @[Top.scala 113:11]
        when _T_28 : @[Top.scala 113:11]
          printf(clock, UInt<1>("h1"), "Assumption failed\n    at Top.scala:113 assume(!mark_vld)\n") : printf_4 @[Top.scala 113:11]
        assume(clock, _T_25, UInt<1>("h1"), "") : assume_4 @[Top.scala 113:11]
    when check_vld : @[Top.scala 116:18]
      when resetCounter.notChaos : @[Top.scala 117:11]
        node _T_29 = bits(reset, 0, 0) @[Top.scala 117:11]
        node _T_30 = eq(_T_29, UInt<1>("h0")) @[Top.scala 117:11]
        when _T_30 : @[Top.scala 117:11]
          node _T_31 = eq(flag, UInt<1>("h0")) @[Top.scala 117:11]
          when _T_31 : @[Top.scala 117:11]
            printf(clock, UInt<1>("h1"), "Assertion failed: \n    at Formal.scala:20 cassert(cond, msg)\n") : printf_5 @[Top.scala 117:11]
          assert(clock, flag, UInt<1>("h1"), "") : assert @[Top.scala 117:11]

